import formula.BinaryFormula;
import formula.Formula;
import proof.ConclusionProof;
import proof.Proof;
import proof.ProofRule;
import proof.DerivedProof;
import sign.FormulaSign;

import java.util.*;

public class Solve {
    private static void appendResult(ArrayList<Proof> res,Proof proof){
        for (Proof p:res) {
            if (p.getConclusion().equals(proof.getConclusion())){
                return;
            }
        }
        res.add(proof);
    }

    //D1 apply
    private static ArrayList<Proof> applyD1(ArrayList<Proof> conditions, UsedCondition usedConditions){
        ArrayList<Proof> res=(ArrayList<Proof>) conditions.clone();
        for (Proof p1:conditions){
            for (Proof p2:conditions){
                ArrayList<Proof> ps = new ArrayList<>();
                ps.add(p1);
                ps.add(p2);
                if (!usedConditions.contain(ps,ProofRule.D1)) {
                    if (ProofRule.D1.applyRule(ps) != null) {
                        appendResult(res,new DerivedProof(ps, ProofRule.D1));
                        usedConditions.add(ps,ProofRule.D1);
                    }
                }
            }

        }
        return res;
    }

    //B apply
    private static ArrayList<Proof> applyB(ArrayList<Proof> conditions, UsedCondition usedConditions){
        ArrayList<Proof> res=(ArrayList<Proof>) conditions.clone();
        for (Proof p1:conditions){
            for (Proof p2:conditions){
                ArrayList<Proof> ps = new ArrayList<>();
                ps.add(p1);
                ps.add(p2);
                if (!usedConditions.contain(ps,ProofRule.B)) {
                    if (ProofRule.B.applyRule(ps) != null) {
                        appendResult(res,new DerivedProof(ps, ProofRule.B));
                        usedConditions.add(ps,ProofRule.B);
                    }
                }
            }

        }
        return res;
    }

    //D2 apply
    private static ArrayList<Proof> applyD2(ArrayList<Proof> conditions, UsedCondition usedConditions){
        ArrayList<Proof> res=(ArrayList<Proof>) conditions.clone();
        //System.out.println(usedConditions);

        for (Proof p1:conditions){
            for (Proof p2:conditions){
                ArrayList<Proof> ps = new ArrayList<>();
                ps.add(p1);
                ps.add(p2);

                if (!usedConditions.contain(ps,ProofRule.D2)) {
//                    System.out.println("p1 result: "+p1.getConclusion().toString());
//                    System.out.println("p2 result: "+p2.getConclusion().toString());
                    if (ProofRule.D2.applyRule(ps) != null) {
                        appendResult(res,new DerivedProof(ps, ProofRule.D2));
                        usedConditions.add(ps,ProofRule.D2);
                    }
                }
            }
        }
        return res;
    }
    //D3 apply
    private static ArrayList<Proof> applyD3(ArrayList<Proof> conditions, UsedCondition usedConditions){
        ArrayList<Proof> res=(ArrayList<Proof>) conditions.clone();
        for (Proof p1:conditions){
            for (Proof p2:conditions){
                ArrayList<Proof> ps = new ArrayList<>();
                ps.add(p1);
                ps.add(p2);
                if (!usedConditions.contain(ps,ProofRule.D3)) {
                    if (ProofRule.D3.applyRule(ps) != null) {
                        appendResult(res,new DerivedProof(ps, ProofRule.D3));
                        usedConditions.add(ps,ProofRule.D3);
                    }
                }
            }
        }
        return res;
    }

    //I apply
    private static ArrayList<Proof> applyI(ArrayList<Proof> conditions, UsedCondition usedConditions){
        ArrayList<Proof> res=(ArrayList<Proof>) conditions.clone();
        for (Proof proof:conditions){
            ArrayList<Proof> ps = new ArrayList<>();
                ps.add(proof);
                if (!usedConditions.contain(ps,ProofRule.I)) {
                    if (ProofRule.I.applyRule(ps) != null) {
                        appendResult(res,new DerivedProof(ps, ProofRule.I));
                        usedConditions.add(ps,ProofRule.I);
                    }
                }
            }
        return res;
    }

    //A apply
    private static ArrayList<Proof> applyA(ArrayList<Proof> conditions, UsedCondition usedConditions){
        ArrayList<Proof> res=(ArrayList<Proof>) conditions.clone();
        for (Proof proof:conditions){
            ArrayList<Proof> ps = new ArrayList<>();
            ps.add(proof);
            if (!usedConditions.contain(ps,ProofRule.A)) {
                if (ProofRule.A.applyRule(ps) != null) {
                    appendResult(res,new DerivedProof(ps, ProofRule.A));
                    usedConditions.add(ps,ProofRule.A);
                }
            }
        }
        return res;
    }


    //TF专属规则
    //ANY-ANY rule
    private static ArrayList<Proof> applyAA(ArrayList<Proof> conditions, UsedCondition usedConditions){
        ArrayList<Proof> res=(ArrayList<Proof>) conditions.clone();
        for (Proof p1:conditions){
            for (Proof p2:conditions){
                ArrayList<Proof> ps = new ArrayList<>();
                ps.add(p1);
                ps.add(p2);
                if (!usedConditions.contain(ps,ProofRule.AA)) {
                    if (ProofRule.AA.applyRule(ps) != null) {
                        appendResult(res,new DerivedProof(ps, ProofRule.AA));
                        usedConditions.add(ps,ProofRule.AA);
                    }
                }
            }
        }
        return res;
    }

    //EXIST-EXIST rule
    private static ArrayList<Proof> applyEE(ArrayList<Proof> conditions, UsedCondition usedConditions){
        ArrayList<Proof> res=(ArrayList<Proof>) conditions.clone();
        for (Proof p1:conditions){
            for (Proof p2:conditions){
                ArrayList<Proof> ps = new ArrayList<>();
                ps.add(p1);
                ps.add(p2);
                if (!usedConditions.contain(ps,ProofRule.EE)) {
                    if (ProofRule.EE.applyRule(ps) != null) {
                        appendResult(res,new DerivedProof(ps, ProofRule.EE));
                        usedConditions.add(ps,ProofRule.EE);
                    }
                }
            }
        }
        return res;
    }

    //AE rule
    private static ArrayList<Proof> applyAE(ArrayList<Proof> conditions, UsedCondition usedConditions){
        ArrayList<Proof> res=(ArrayList<Proof>) conditions.clone();
        for (Proof p1:conditions){
            for (Proof p2:conditions){
                ArrayList<Proof> ps = new ArrayList<>();
                ps.add(p1);
                ps.add(p2);
                if (!usedConditions.contain(ps,ProofRule.AE)) {
                    if (ProofRule.AE.applyRule(ps) != null) {
                        appendResult(res,new DerivedProof(ps, ProofRule.AE));
                        usedConditions.add(ps,ProofRule.AE);
                    }
                }
            }
        }
        return res;
    }



    //II apply
    private static ArrayList<Proof> applyII(ArrayList<Proof> conditions, UsedCondition usedConditions){
        ArrayList<Proof> res=(ArrayList<Proof>) conditions.clone();
        for (Proof proof:conditions){
            ArrayList<Proof> ps = new ArrayList<>();
            ps.add(proof);
            if (!usedConditions.contain(ps,ProofRule.II)) {

                if (ProofRule.II.applyRule(ps) != null) {
                    DerivedProof proof1=new DerivedProof(ps, ProofRule.II);
                    appendResult(res,proof1);
                    usedConditions.add(ps,ProofRule.II);
                }
            }
        }
        return res;
    }


    /*
    applyRAA(ArrayList<Proof> conditions, Formula conclusion, UsedCondition usedConditions){
        if (conclusion is bottom) {
            return null;
        }

        conditions.add(xxxx);
        Formula bottom = xxx;
        return solveHelper(conditions, conclusion, usedConditions);
    }

     */
    public static Proof solveHelper(ArrayList<Proof> conditions, Formula conclusion, UsedCondition usedConditions){
        //TODO
//        if (applyX(conditions)){
//            System.out.println("Rule X is applied!");
//            System.out.println("The result will be true.Program finishes.");
//            return null;
//        }else {
//
//        }
//        for (Proof condition:conditions){
//            System.out.println(condition.toLatex());
//        }
//        System.out.println("-------------");
//        System.out.println("applyD1");
        ArrayList<Proof> newConditions=applyD1(conditions, usedConditions);
//        System.out.println("applyB");
        newConditions=applyB(newConditions,usedConditions);
//        System.out.println("applyD2");
        newConditions=applyD2(newConditions,usedConditions);
  //      System.out.println("applyD3");
        newConditions=applyD3(newConditions,usedConditions);
    //    System.out.println("applyI");
        newConditions=applyI(newConditions,usedConditions);
        //newConditions=applyT(newConditions,usedConditions);
      //  System.out.println("applyA");
        newConditions=applyA(newConditions,usedConditions);
      //  System.out.println("applyAA");
        newConditions=applyAA(newConditions,usedConditions);
      //  System.out.println("applyEE");
        newConditions=applyEE(newConditions,usedConditions);
      //  System.out.println("applyAE");
        newConditions=applyAE(newConditions,usedConditions);
      //  System.out.println("applyII");
        newConditions=applyII(newConditions,usedConditions);
        //newConditions=applyContradiction(conditions, usedConditions);

        //证明成功
        for (Proof condition:newConditions){
            //System.out.println(condition);
            if (condition.getConclusion().equals(conclusion)){
                return condition;
            }

        }
        //System.out.println(" ");

        if (newConditions.size()==conditions.size()){//没有新的formula生成(no new formula be created)
            //return applyRAA(conditions, conclusion, usedConditions);
            return null;
        }
        return solveHelper(newConditions, conclusion, usedConditions);
    }



    public static Proof solve(ArrayList<Formula> formulas,Formula conclusion) {
        //TODO
        ArrayList<Proof> conditions = new ArrayList<>();
        Set<Formula> tset=new HashSet<>();

        for (Formula f : formulas) {
            BinaryFormula bf=(BinaryFormula) f;//此时的输入应该都为bf，可以进行类型转换
            tset.add(bf.getLeft());
            tset.add(bf.getRight());
            conditions.add(new ConclusionProof(f));
        }
        for (Formula formula:tset) {//对tSet中的元素依次应用TRules
            //System.out.println(formula);
            BinaryFormula result=new BinaryFormula(FormulaSign.ANY,formula,formula);
            conditions.add(new ConclusionProof(result));
        }

        return solveHelper(conditions, conclusion, new UsedCondition());
    }
}


